/LMAR=0/XLINE=3/FONT#0=BAXL30/FONT#1=BAXI30[  J,RED]/FONT#2=BAXB30/FONT#3=NGB30



␈↓ α∧␈↓␈↓ ∧∪␈↓αRunnable Specification As a Design Tool␈↓↓







␈↓ α∧␈↓There are at least four phases in the development of "correct" software.

␈↓ α∧␈↓1)␈α⊃Understanding␈α⊃the␈α⊃problem.␈α⊃ The␈α⊂program␈α⊃designer␈α⊃may␈α⊃work␈α⊃with␈α⊂intended

␈↓ α∧␈↓users␈α∩of␈α∪the␈α∩system␈α∩to␈α∪develop␈α∩an␈α∩intuitive␈α∪understanding␈α∩of␈α∩the␈α∪problem␈α∩and

␈↓ α∧␈↓possible approaches to its solution.

␈↓ α∧␈↓2)␈α∪Formal␈α∩specification.␈α∪ Once␈α∪the␈α∩designer␈α∪knows␈α∪intuitively␈α∩how␈α∪to␈α∪solve␈α∩the

␈↓ α∧␈↓problem, the solution must be specified unambiguously.

␈↓ α∧␈↓3) Programming.  An implementation of the specification is programmed.

␈↓ α∧␈↓4)␈αVerification.␈α The␈αimplementation␈αdeveloped␈αin␈αstep␈αthree␈αis␈αshown␈αto␈αsatisfy␈αthe

␈↓ α∧␈↓formal specification of step two.

␈↓ α∧␈↓There␈α∞is␈α
a␈α∞certain␈α∞amount␈α
of␈α∞testing␈α
and␈α∞debugging␈α∞that␈α
goes␈α∞on␈α
at␈α∞each␈α∞of␈α
these

␈↓ α∧␈↓stages␈αuntil␈αone␈αis␈αsatisfied␈αwith␈αthe␈αcurrent␈αstep␈αand␈αmoves␈αon␈αto␈αthe␈αnext.␈α Several

␈↓ α∧␈↓verification␈α⊂techniques␈α⊂have␈α⊂been␈α⊂developed␈α∂to␈α⊂assist␈α⊂in␈α⊂accomplishing␈α⊂step␈α∂four.

␈↓ α∧␈↓However,␈α∩even␈α∩after␈α∩a␈α∩proof␈α∩is␈α∩completed␈α∩we␈α∩cannot␈α∩claim␈α∩to␈α∩have␈α∩a␈α⊃"correct"

␈↓ α∧␈↓program, only one that satisfies the given specification.

␈↓ α∧␈↓Rather␈α
than␈α
write␈α
a␈α
program,␈α
being␈α
guided␈α
by␈α
the␈α
specification,␈α
and␈α
then␈α
prove␈αit

␈↓ α∧␈↓satisfies␈α∀the␈α∪specifications,␈α∀one␈α∀can␈α∪automatically␈α∀generate␈α∪a␈α∀program␈α∀from␈α∪the

␈↓ α∧␈↓specifications␈αthat␈αis␈αguaranteed␈αto␈α
preserve␈αthe␈αsemantics,␈αthus␈αobviatiing␈α
the␈αneed

␈↓ α∧␈↓for the verification step entirely.

␈↓ α∧␈↓The␈αtruly␈αcreative␈α(and␈α
most␈αdifficult)␈αstep␈αin␈αthe␈α
development␈αof␈αa␈αprogram␈α
is␈αthe



␈↓ α∧␈↓construction␈α
of␈α
an␈α
acceptable␈α
formal␈α
specification␈α
from␈α
an␈α
intuitive␈αunderstanding␈α
of

␈↓ α∧␈↓the␈αproblem.␈α Thus,␈αour␈αefforts␈αshould␈αbe␈αplaced␈αon␈αdeveloping␈αdesign␈αtools␈αto␈αhelp

␈↓ α∧␈↓with the construction and testing of the specification.

␈↓ α∧␈↓How␈α∞does␈α∞one␈α∞"debug"␈α∞a␈α∞specification?␈α∞ We␈α∞cannot␈α∞hope␈α∞to␈α∞formally␈α∞prove␈α∂that␈α∞a

␈↓ α∧␈↓specification␈α
is␈α"correct"␈α
with␈αrespect␈α
to␈αour␈α
intuition,␈α
but␈αwe␈α
can␈αat␈α
least␈αtest␈α
it␈αto␈α
see

␈↓ α∧␈↓that it conforms to our intuition in specific cases.

␈↓ α∧␈↓Guttag␈α
and␈α
Horning␈α
[1]␈α
present␈α
an␈α
algebraic␈α
specification␈α
technique␈α
as␈α
a␈αdesign␈α
tool.

␈↓ α∧␈↓As␈αan␈αexample␈αthey␈αdescribe␈αpart␈α
of␈αthe␈αspecification␈αof␈αa␈αhigh-level␈αinterface␈α
to␈αa

␈↓ α∧␈↓flexible␈α∂display␈α∂and␈α∂discuss␈α∞the␈α∂analysis␈α∂of␈α∂the␈α∞specification.␈α∂ A␈α∂salient␈α∂feature␈α∞of

␈↓ α∧␈↓their␈α
approach␈α
is␈α
the␈α
ability␈α
to␈α
"ask␈α
questions"␈α
of␈α
the␈α
specification,␈α
derive␈α
answers,

␈↓ α∧␈↓and␈α
change␈α
the␈αdesign␈α
if␈α
the␈α
answers␈αare␈α
unacceptable.␈α
 In␈α
this␈αway␈α
they␈α
hope␈αto␈α
test

␈↓ α∧␈↓and debug the specification.

␈↓ α∧␈↓I␈α∞suggest␈α∞that␈α∂Horn␈α∞clauses␈α∞provide␈α∞a␈α∂much␈α∞better␈α∞specification␈α∞language␈α∂than␈α∞do

␈↓ α∧␈↓algebraic␈α∂axioms.␈α⊂ The␈α∂two␈α⊂languages␈α∂are␈α⊂closely␈α∂related;␈α⊂it␈α∂is␈α⊂a␈α∂simple␈α⊂matter␈α∂to

␈↓ α∧␈↓translate␈αbetween␈αthem.␈α
 The␈αease␈αof␈αwriting␈α
a␈αspecification␈αin␈αone␈α
language␈αversus

␈↓ α∧␈↓the␈α∞other␈α∞is␈α∞undoubtedly␈α
a␈α∞matter␈α∞of␈α∞personal␈α
taste␈α∞and␈α∞depends␈α∞largely␈α∞on␈α
which

␈↓ α∧␈↓language␈αone␈α
is␈αmore␈α
familiar␈αwith.␈α
 The␈αsame␈α
may␈αbe␈α
said␈αof␈α
the␈αreadability␈α
of␈αa

␈↓ α∧␈↓specification.␈α Horn␈αclauses,␈α
as␈αwell␈αas␈α
algebraic␈αaxioms,␈αcan␈α
be␈αanalyzed␈αfor␈α
answers

␈↓ α∧␈↓to specific questions and modified accordingly.

␈↓ α∧␈↓The␈α∞major␈α
distinction␈α∞between␈α
the␈α∞two␈α∞methods␈α
is␈α∞the␈α
manner␈α∞in␈α∞which␈α
questions

␈↓ α∧␈↓can␈αbe␈αhandled.␈α
 With␈αthe␈αGuttag-Horning␈αapproach,␈α
an␈αinformal␈αquestion␈αis␈α
posed

␈↓ α∧␈↓and␈α∞submitted␈α∞to␈α∂an␈α∞"expert"␈α∞who␈α∞reformulates␈α∂the␈α∞question,␈α∞often␈α∂generalizing␈α∞it.

␈↓ α∧␈↓The␈αquestioner␈αmust␈αthen␈αbe␈αconvinced␈αthat␈αthe␈αformal␈αstatement␈αdeveloped␈αby␈αthe



␈↓ α∧␈↓expert␈α∪does␈α∪indeed␈α∪reflect␈α∪the␈α∀original␈α∪question,␈α∪and␈α∪an␈α∪answer␈α∪to␈α∀the␈α∪formal

␈↓ α∧␈↓question␈α
will␈α
provide␈α
an␈α
answer␈α
to␈α
the␈α
informal␈α
one.␈α
 Then␈α
an␈α
attempt␈α
is␈α
made␈αto

␈↓ α∧␈↓derive an answer from the axioms.

␈↓ α∧␈↓The␈αsame␈αapproach␈αmay␈αbe␈αtaken␈α
with␈αHorn␈αclauses,␈αbut␈αit␈αis␈αnot␈α
necessary.␈α Since

␈↓ α∧␈↓Horn␈α⊃clauses␈α⊃may␈α∩be␈α⊃run,␈α⊃if␈α∩the␈α⊃questioner␈α⊃wants␈α⊃to␈α∩know␈α⊃what␈α⊃happens␈α∩in␈α⊃a

␈↓ α∧␈↓particular␈α
case,␈α
it␈α
is␈α
possible␈α
to␈α
simply␈α"try␈α
it␈α
and␈α
see".␈α
The␈α
expert␈α
will␈α
still␈αbe␈α
needed

␈↓ α∧␈↓to␈αdevelop␈αthe␈αspecification␈αand␈αto␈αdetermine␈αwhat␈αmodifications␈αshould␈αbe␈αmade␈αto

␈↓ α∧␈↓the␈α∂specification␈α∞to␈α∂change␈α∞an␈α∂unacceptable␈α∞answer,␈α∂but␈α∞the␈α∂"what␈α∞happens␈α∂if␈α∞...?"

␈↓ α∧␈↓questions no longer need be formalized.

␈↓ α∧␈↓Once␈αone␈αis␈αsatisfied␈αthat␈αa␈α
Horn␈αclause␈αspecification␈αis␈αa␈αreasonable␈αembodiment␈α
of

␈↓ α∧␈↓one's␈α∞intuition,␈α∞the␈α∞task␈α∞of␈α∞refining␈α
the␈α∞specification␈α∞into␈α∞an␈α∞efficient␈α∞program␈α
can

␈↓ α∧␈↓proceed.␈α∀The␈α∀ability␈α∀to␈α∪run␈α∀a␈α∀specification␈α∀makes␈α∪the␈α∀problem␈α∀of␈α∀testing␈α∪and

␈↓ α∧␈↓debugging it much more tractable.

␈↓ α∧␈↓As␈αan␈αexample,␈αI␈αhave␈αwritten␈αthe␈αHorn␈αclause␈αspecification␈αof␈αthe␈αdisplay␈αspecified

␈↓ α∧␈↓with␈αalgebraic␈αasioms␈α
by␈αGuttag␈αand␈αHorning.␈α
 The␈αfundamental␈αassumption␈αis␈α
that

␈↓ α∧␈↓a␈α
user␈α
will␈α
want␈α
to␈α
be␈α
able␈α
to␈α
display␈α
several␈α
distinct␈α
blocks␈α
of␈α
information␈α
on␈αthe

␈↓ α∧␈↓screen␈α∪at␈α∩once.␈α∪ The␈α∪top␈α∩level␈α∪concept␈α∪is␈α∩that␈α∪of␈α∩a␈α∪view␈↓↓.␈α∪A␈α∩␈↓view␈↓↓␈α∪is␈α∪a␈α∩spatial

␈↓ α∧␈↓↓arrangement␈α⊃of␈α⊃␈↓pictures␈↓↓;␈α⊂a␈α⊃␈↓picture␈↓↓␈α⊃is␈α⊂a␈α⊃block␈α⊃of␈α⊂displayble␈α⊃information.␈α⊃A␈α⊂picture

␈↓ α∧␈↓↓consists␈α∞of␈α∞a␈α∞boundary,␈α∞a␈α∞contents,␈α∞and␈α∞a␈α∞coordinate␈α∞transformation␈α∞to␈α∞be␈α∂applied␈α∞in

␈↓ α∧␈↓↓viewing␈α∀its␈α∪contents.␈α∀Examples␈α∀of␈α∪pictures␈α∀are␈α∀the␈α∪entire␈α∀display␈α∀(with␈α∪implicit

␈↓ α∧␈↓↓boundary),␈α
and␈α
the␈α
interior␈α
of␈α
a␈α
fixed␈α
rectangle␈α
on␈α
the␈α
display;␈α
examples␈α
of␈α
contents

␈↓ α∧␈↓↓are text, figures, and views.

␈↓ α∧␈↓↓The Guttag-Horning specification of picture is as follows:

␈↓ α∧␈↓↓␈↓Operators:



␈↓ α∧␈↓MakePicture: Contents ␈↓βX␈↓ [Coordinate → TruthValues] ␈↓βX␈↓ [Coordinate → Coordinate]
␈↓ α∧␈↓                                 → Picture

␈↓ α∧␈↓Picture.Appearance: Picture ␈↓βX␈↓ Coordinate → Illumination

␈↓ α∧␈↓Picture.In: Picture ␈↓βX␈↓ Coordinate → TruthValues

␈↓ α∧␈↓Axioms:

␈↓ α∧␈↓Picture.Appearance(MakePicture(cont, bound, trans), coord)
␈↓ α∧␈↓                                        = Contents.Appearance(cont, trans(coord))

␈↓ α∧␈↓Picture.In(MakePicture(cont, bound, trans), coord) = bound(coord)


␈↓ α∧␈↓↓The␈α⊂operators␈α⊂are␈α⊃listed␈α⊂first,␈α⊂giving␈α⊂their␈α⊃functionality,␈α⊂then␈α⊂the␈α⊃axioms␈α⊂defining

␈↓ α∧␈↓↓them␈αare␈αgiven.␈α ␈↓MakePicture␈↓↓␈αis␈αnot␈αdefined␈αfurther␈αsince␈αit␈αis␈αsimply␈αthe␈αconstructor

␈↓ α∧␈↓↓function␈αfor␈αthe␈αtype␈α␈↓Picture␈↓↓.␈α The␈αfirst␈αaxiom␈αtells␈αus␈αthat␈αthe␈αappearance␈αat␈αa␈α
given

␈↓ α∧␈↓↓coordinate␈αin␈αa␈α␈↓picture␈↓↓␈αis␈αdetermined␈α
by␈αthe␈αappearance␈αat␈αa␈αcoordinate␈α(the␈α
result␈αof

␈↓ α∧␈↓↓applying␈αthe␈αtransformation␈αto␈αthe␈αoriginal␈αcoordinate)␈αin␈αthe␈α␈↓contents␈↓↓␈αof␈αthe␈α␈↓picture␈↓↓.

␈↓ α∧␈↓↓The␈α∩second␈α∩axiom␈α∩indicates␈α∩that␈α∩a␈α∩coordinate␈α⊃is␈α∩in␈α∩a␈α∩␈↓picture␈↓↓␈α∩if␈α∩it␈α∩is␈α∩within␈α⊃the

␈↓ α∧␈↓↓boundary of the ␈↓picture␈↓↓ as defined by the function ␈↓bound␈↓↓.

␈↓ α∧␈↓↓The␈αspecification␈αof␈αtype␈α␈↓Picture␈↓↓␈αusing␈αHorn␈αclauses␈αis␈αgiven␈αbelow.␈αThe␈αHorn␈αclause

␈↓ α∧␈↓↓specification␈α⊂clearly␈α⊃indicates␈α⊂the␈α⊃distinction␈α⊂between␈α⊃constructor␈α⊂functions,␈α⊃such␈α⊂as

␈↓ α∧␈↓↓␈↓make-picture␈↓↓,␈α
and␈αthe␈α
predicates␈α
indicating␈αrelationships␈α
among␈α
their␈αarguments.␈α
The

␈↓ α∧␈↓↓type␈α⊃constraints,␈α∩indicating␈α⊃functionality␈α⊃of␈α∩the␈α⊃predicates,␈α⊃are␈α∩given␈α⊃only␈α∩for␈α⊃the

␈↓ α∧␈↓↓clause(s)␈α
defining␈α
the␈αtype␈α
being␈α
specified.␈α Type-checking␈α
can␈α
be␈α
included␈αexplicitly

␈↓ α∧␈↓↓in␈α∂each␈α⊂clause,␈α∂however,␈α⊂we␈α∂assume␈α⊂the␈α∂required␈α⊂type␈α∂is␈α⊂made␈α∂obvious␈α⊂by␈α∂consistent

␈↓ α∧␈↓↓naming␈α
of␈α
variables␈α
and␈α
choose␈α
to␈α
leave␈α
it␈α
out␈α
of␈α
the␈α
rest␈α
of␈α
the␈α
specification␈α
for␈α
the

␈↓ α∧␈↓↓sake of readability.

␈↓ α∧␈↓↓␈↓Picture(make-picture(cont, bound, trans)) ← Contents(cont), Boundary(bound),
␈↓ α∧␈↓                                                Translation(trans)



␈↓ α∧␈↓Picture-Appearance(make-picture(cont, bound, trans), coord, illum) ←
␈↓ α∧␈↓        Compute-position(coord,trans,coord'), Contents-appearance(cont, coord'),

␈↓ α∧␈↓Picture-In(make-picture(cont, bound, trans), coord, tv) ← Lies-in(coord, bound, tv)


␈↓ α∧␈↓↓In␈α∪the␈α∀Guttag-Horning␈α∪axiomatic␈α∀specification␈α∪of␈α∀the␈α∪display,␈α∀a␈α∪␈↓boundary␈↓↓␈α∀is␈α∪a

␈↓ α∧␈↓↓function␈α∪from␈α∪␈↓Coordinate␈↓↓␈α∪to␈α∪␈↓TruthValues␈↓↓␈α∪and␈α∪a␈α∪␈↓translation␈↓↓␈α∪is␈α∪a␈α∪function␈α∩from

␈↓ α∧␈↓↓␈↓Coordinate␈↓↓␈α
to␈α
␈↓Coordinate␈↓↓.␈α Horn␈α
clause␈α
syntax␈α
does␈αnot␈α
allow␈α
functions␈αas␈α
arguments,

␈↓ α∧␈↓↓thus␈α∂I've␈α∂treated␈α∂␈↓trans␈↓↓␈α∞and␈α∂␈↓bound␈↓↓␈α∂as␈α∂objects,␈α∞␈↓Compute-position␈↓↓␈α∂is␈α∂a␈α∂predicate␈α∞that

␈↓ α∧␈↓↓accomplishes␈α∂the␈α∂translation␈α∂from␈α∂␈↓coord␈↓↓␈α∂to␈α∂␈↓coord'␈↓↓␈α∂indicated␈α∂by␈α∂the␈α∂Guttag-Horning

␈↓ α∧␈↓↓␈↓trans␈↓↓,␈α
similarly,␈α␈↓Lies-in(coord,␈α
bound,␈αtv)␈↓↓␈α
results␈αin␈α
␈↓tv␈↓↓␈α
being␈αbound␈α
to␈α␈↓true␈↓↓␈α
if␈αand␈α
only

␈↓ α∧␈↓↓if␈α⊂the␈α⊂Guttag-Horning␈α⊂␈↓bound(coord)␈↓↓␈α⊂is␈α⊂␈↓true␈↓↓,␈α⊃and␈α⊂to␈α⊂␈↓false␈↓↓␈α⊂if␈α⊂and␈α⊂only␈α⊃if␈α⊂Guttag-

␈↓ α∧␈↓↓Horning␈α∂␈↓bound(coord)␈↓↓␈α∂is␈α∞␈↓false␈↓↓.␈α∂ I␈α∂would␈α∞not␈α∂need␈α∂the␈α∂predicates␈α∞␈↓Compute-position␈↓↓

␈↓ α∧␈↓↓and␈α∪␈↓Lies-in␈↓↓␈α∪if␈α∪I␈α∪had␈α∪an␈α∪evaluation␈α∪predicate␈α∪which␈α∪accepts␈α∪a␈α∪function␈α∪and␈α∩its

␈↓ α∧␈↓↓arguments␈α
and␈α
applies␈α
the␈α
function␈α
to␈α
the␈α
arguments,␈α
such␈α
as␈α
the␈α
LISP␈α∞"apply".␈α
 I

␈↓ α∧␈↓↓have␈α⊃decided␈α⊂to␈α⊃remain␈α⊂within␈α⊃first-order␈α⊃logic␈α⊂and␈α⊃the␈α⊂strict␈α⊃limitations␈α⊃of␈α⊂Horn

␈↓ α∧␈↓↓clauses.␈α Others␈αhave␈αconcerned␈αthemselves␈αwith␈αthe␈αproblem␈αof␈αmoving␈αto␈α
second-order,

␈↓ α∧␈↓↓as shown in the "demonstrate" predicate used by Ken Bowen and Alan Robinson.

␈↓ α∧␈↓↓The specification of type ␈↓View␈↓↓, given algebraically, is as follows:

␈↓ α∧␈↓↓␈↓Operators:

␈↓ α∧␈↓View.Empty: → View

␈↓ α∧␈↓AddPicture: View ␈↓βX␈↓ Coordinate ␈↓βX␈↓ PictureId ␈↓βX␈↓ Picture → View

␈↓ α∧␈↓View.Appearance: View ␈↓βX␈↓ Coordinate → Illumination

␈↓ α∧␈↓View.In: View ␈↓βX␈↓ Coordinate → TruthValues

␈↓ α∧␈↓FindPictures: View ␈↓βX␈↓ Coordinate → IdList

␈↓ α∧␈↓DeletePicture: View ␈↓βX␈↓ PictureId → View



␈↓ α∧␈↓Axioms:

␈↓ α∧␈↓View.Appearance(AddPicture(v, coord', id, p), coord) =
␈↓ α∧␈↓                ␈↓↓if␈↓ Picture.In(p, Minus(coord, coord'))
␈↓ α∧␈↓                ␈↓↓then␈↓ Picture.Appearance(p, Minus(coord, coord'))
␈↓ α∧␈↓                ␈↓↓else␈↓ View.Appearance(v, coord)

␈↓ α∧␈↓View.Appearance(View.Empty, coord)␈↓↓ intentionally left unspecified

␈↓ α∧␈↓↓␈↓View.In(View.Empty, coord) = False

␈↓ α∧␈↓View.In(AddPicture(v, coord', id, p), coord) =
␈↓ α∧␈↓                        Picture.In(p, Minus(coord, coord')) ∨ View.In(v, coord)

␈↓ α∧␈↓FindPictures(View.Empty, coord) = IdList.Empty

␈↓ α∧␈↓FindPictures(AddPicture(v, coord', id, p), coord) =
␈↓ α∧␈↓                ␈↓↓if␈↓ Picture.In(p, Minus(coord, coord'))
␈↓ α∧␈↓                ␈↓↓then␈↓ IdList.Insert(id, FindPictures(v, coord))
␈↓ α∧␈↓                ␈↓↓else␈↓ FindPictures(v, coord)

␈↓ α∧␈↓DeletePicture(View.Empty, id) = View.Empty

␈↓ α∧␈↓DeletePicture( AddPicture(v, coord, id', p), id) =
␈↓ α∧␈↓                ␈↓↓if␈↓ PictureId.Equal(id, id')
␈↓ α∧␈↓                ␈↓↓then␈↓ v
␈↓ α∧␈↓                ␈↓↓else␈↓ AddPicture(DeletePicture(v, id), coord, id', p)


␈↓ α∧␈↓↓Guttag␈αand␈αHorning␈α
use␈αthe␈αconvention␈αof␈α
prefixing␈αa␈αfunction␈αname␈α
by␈αthe␈αtype␈αit␈α
is

␈↓ α∧␈↓↓operating␈αon␈αand␈αa␈α
dot.␈α In␈αthis␈αway␈α
they␈αcan␈αuse␈αthe␈α
same␈αname␈αfor␈αsimilar␈α
functions

␈↓ α∧␈↓↓being␈α∀defined␈α∀over␈α∪several␈α∀different␈α∀types.␈α∪ They␈α∀chose␈α∀to␈α∪use␈α∀a␈α∀0-ary␈α∪function

␈↓ α∧␈↓↓␈↓View.Empty␈↓↓␈αto␈α
indicate␈αthe␈α
empty␈αview,␈α
we␈αuse␈α
a␈αconstant␈α
␈↓mt-view␈↓↓.␈α␈↓AddPicture␈↓↓␈αis␈α
the

␈↓ α∧␈↓↓constructor␈α∀function␈α∀for␈α∀type␈α∀␈↓View␈↓↓.␈α∀ ␈↓Appearance␈↓↓␈α∀and␈α∀␈↓In␈↓↓␈α∀are␈α∀determined␈α∀by␈α∪the

␈↓ α∧␈↓↓components␈α(pictures)␈α
making␈αup␈α
a␈αview.␈α ␈↓FindPictures␈↓↓␈α
is␈αa␈α
function␈αthat␈αconstructs␈α
a

␈↓ α∧␈↓↓list␈αof␈α
␈↓id␈↓↓'s␈αof␈αpictures␈α
containing␈αa␈αgiven␈α
coordinate.␈α ␈↓DeletePicture␈↓↓␈αdeletes␈α
a␈αpicture,

␈↓ α∧␈↓↓specified by its ␈↓id␈↓↓, from a view.

␈↓ α∧␈↓↓Again,␈α_using␈α↔Horn␈α_clauses,␈α↔we␈α_indicate␈α↔the␈α_types␈α↔of␈α_arguments␈α↔only␈α_in␈α↔the



␈↓ α∧␈↓↓specification␈αof␈α␈↓View␈↓↓,␈αand␈αassume␈αthe␈αdesired␈αtypes␈αare␈αmade␈αapparent␈αby␈αnaming␈αof

␈↓ α∧␈↓↓variables.

␈↓ α∧␈↓↓␈↓View(mt-view) ←

␈↓ α∧␈↓View(addpicture(v, c, id, p)) ← View(v), Coordinate(c), PictureId(id), Picture(p)

␈↓ α∧␈↓View-Appearance(mt-view, coord, x) ←

␈↓ α∧␈↓␈↓↓As in the algebraic specification, we leave unspecified the appearance of the
␈↓ α∧␈↓↓mt-view at any coordinate.  Since we have no if-then-else, the axiom describing
␈↓ α∧␈↓↓␈↓View.Appearance␈↓↓ corresponds to two Horn clauses, one for each alternative.␈↓

␈↓ α∧␈↓View-Appearance(addpicture(v, coord', id, p), coord, illum) ←
␈↓ α∧␈↓                                Picture-In(p, minus(coord, coord'), true),
␈↓ α∧␈↓                                Picture-Appearance(p, minus(coord, coord'), illum)

␈↓ α∧␈↓View-Appearance(addpicture(v, coord', id, p), coord, illum) ←
␈↓ α∧␈↓                                Picture-In(p, minus(coord, coord'), false),
␈↓ α∧␈↓                                View-Appearance(v, coord, illum)

␈↓ α∧␈↓View-In(mt-view, coord, false) ←

␈↓ α∧␈↓␈↓↓Horn clauses are not allowed alternative conditions. Thus the second axiom for
␈↓ α∧␈↓↓␈↓View.In␈↓↓ is handled by the following three Horn clauses, one for each alternative
␈↓ α∧␈↓↓making the conclusion ␈↓true␈↓↓, and a third to enable us to derive the fact that a
␈↓ α∧␈↓↓coordinate is not in a ␈↓view␈↓↓.

␈↓ α∧␈↓↓␈↓View-In(addpicture(v, coord', id, p), coord, true) ←
␈↓ α∧␈↓                                Picture-In(p, minus(coord, coord'), true)

␈↓ α∧␈↓View-In(addpicture(v, coord', id, p), coord, true) ← View-In(v, coord, true)

␈↓ α∧␈↓View-In(addpicture(v, coord', id, p), coord, false) ←
␈↓ α∧␈↓                                Picture-In(p, minus(coord, coord'), false),
␈↓ α∧␈↓                                View-In(v, coord, false)

␈↓ α∧␈↓FindPictures(mt-view, coord, mt-idlist) ←

␈↓ α∧␈↓FindPictures(addpicture(v, coord', id, p), coord, idlist-insert(id,idl)) ←
␈↓ α∧␈↓                                Picture-In(p, minus(coord, coord'), true),
␈↓ α∧␈↓                                FindPictures(v, coord, idl)

␈↓ α∧␈↓FindPictures(addpicture(v, coord', id, p), coord, idl) ←
␈↓ α∧␈↓                                Picture-In(p, minus(coord, coord'), false),
␈↓ α∧␈↓                                FindPictures(v, coord, idl)



␈↓ α∧␈↓DeletePicture(mt-view, id, mt-view) ←

␈↓ α∧␈↓DeletePicture(addpicture(v, coord, id, p), id, v) ←

␈↓ α∧␈↓DeletePicture(addpicture(v, coord, id', p), id, addpicture(v', coord, id', p)) ←
␈↓ α∧␈↓                                PictureId-equal(id, id', false),
␈↓ α∧␈↓                                DeletePicture(v, id, v')


␈↓ α∧␈↓↓␈↓FindPictures␈↓↓␈α∂and␈α∞␈↓DeletePicture␈↓↓␈α∂present␈α∞no␈α∂surprises.␈α∞ Again,␈α∂an␈α∞if-then-else␈α∂in␈α∞an

␈↓ α∧␈↓↓axiom␈αresults␈αin␈αtwo␈α
clauses␈αin␈αthe␈αHorn␈α
clause␈αspecification.␈α A␈αcomplete␈αHorn␈α
clause

␈↓ α∧␈↓↓specification of the display is given in the appendix (not included with the abstract).

␈↓ α∧␈↓↓In␈α∞analyzing␈α∞the␈α∞specification␈α∞using␈α∞the␈α
algebraic␈α∞axioms␈α∞one␈α∞needs␈α∞an␈α∞expert␈α∞to␈α
go

␈↓ α∧␈↓↓between␈α⊃the␈α⊃questioner␈α∩and␈α⊃the␈α⊃specification.␈α∩ For␈α⊃example,␈α⊃and␈α∩informal␈α⊃question

␈↓ α∧␈↓↓asked␈αof␈αGuttag␈α
and␈αHorning␈αwas:␈α"Is␈α
it␈αthe␈αcase␈αthat␈α
pictures␈αare␈αnot␈αtransparent␈α
or

␈↓ α∧␈↓↓even␈α∞translucent?␈α∞I.e.,␈α∞if␈α∂two␈α∞pictures␈α∞overlap,␈α∞does␈α∞the␈α∂bottom␈α∞one␈α∞have␈α∞no␈α∂effect␈α∞on

␈↓ α∧␈↓↓what one sees through the top one?". The question was formalized as:

␈↓ α∧␈↓↓"Is it true that
␈↓ α∧␈↓↓␈↓(∀c,c',w,id,v1,v2)[Picture.In(w,Minus(c,c')) →
␈↓ α∧␈↓        [View.Appearance(AddPicture(v1,c',id,w),c)
␈↓ α∧␈↓                        = View.Appearance(AddPicture(v2,c',id,w),c)]] ␈↓↓?"


␈↓ α∧␈↓↓The␈α∃formal␈α∀question␈α∃is␈α∀answered␈α∃affirmatively,␈α∀following␈α∃directly␈α∀from␈α∃the␈α∀first

␈↓ α∧␈↓↓alternative in the first axiom of type ␈↓View␈↓↓.

␈↓ α∧␈↓↓If␈α∪we␈α∩so␈α∪desired,␈α∩we␈α∪could␈α∩formalize␈α∪the␈α∩question␈α∪to␈α∩be␈α∪put␈α∩to␈α∪our␈α∪Horn␈α∩clause

␈↓ α∧␈↓↓specification␈αand␈αderive␈αthe␈αsame␈αanswer,␈αusing␈αthe␈αsecond␈αclause␈αin␈αthe␈αdefinition␈αof

␈↓ α∧␈↓↓␈↓View-Appearance␈↓↓,␈α⊗but␈α⊗there␈α↔is␈α⊗no␈α⊗need.␈α⊗ Since␈α↔we␈α⊗can␈α⊗run␈α⊗the␈α↔Horn␈α⊗clause

␈↓ α∧␈↓↓specification,␈α∞all␈α∞the␈α∂user␈α∞need␈α∞do␈α∂is␈α∞construct␈α∞overlapping␈α∂pictures␈α∞and␈α∞look␈α∂at␈α∞the

␈↓ α∧␈↓↓result.

␈↓ α∧␈↓↓Using␈α∪Horn␈α∀clauses␈α∪as␈α∪a␈α∀design␈α∪tool␈α∪we␈α∀enjoy␈α∪all␈α∪the␈α∀benefits␈α∪of␈α∀the␈α∪algebraic



␈↓ α∧␈↓↓approach,␈αand␈α
gain␈αthe␈α
advantage␈αthat␈αtesting␈α
is␈αmore␈α
easily␈αaccomplished.␈α An␈α
expert

␈↓ α∧␈↓↓may␈αstill␈αbe␈αrequired␈αto␈αdevelop␈α
the␈αdesign␈αspecification␈αand␈αto␈αmodify␈αit␈α
if␈αnecessary,

␈↓ α∧␈↓↓but␈αthe␈αanalysis␈αof␈αthe␈αdesign␈αcan␈αbe␈αcarried␈αout␈αby␈αpeople␈αwho␈αmay␈αbe␈αexperts␈α
in␈αthe

␈↓ α∧␈↓↓problem domain but not in the specification language.
␈↓ α∧␈↓↓␈↓ ¬c␈↓αReferences␈↓↓

␈↓ α∧␈↓↓[1] Guttag, J., and J. Horning, "Formal Specification As a Design Tool",
␈↓ α∧␈↓↓                Proceedings of the ACM Symposium on Principles of Programming
␈↓ α∧␈↓↓                Languages, 1980.

␈↓ α∧␈↓↓[2] Kowalski, R., ␈↓Logic for Problem Solving, Elsevier North Holland, Inc., 1979.